module Bus

open GPS
open Map
open Time

sig Bus{
	gps: one GPS,
	location: Location -> Time
}

fact everyBusHasDifferentGps{
	all disj b1, b2: Bus | b1.gps != b2.gps
}

fact everyGpsShowsHisBusLocation{
	all g:GPS | all t:Time | some b:Bus | gpsInBus[g,b] and sameLocation[g,b,t]
}

pred gpsInBus[g:GPS, b:Bus]{
	g = b.gps
}

pred sameLocation[g : GPS, b : Bus, t : Time] {
	g.show.t = b.location.t
}

fact busHaveLocation {
	all b:Bus | all t : Time | some l:Location | compareBusLocation[b,l,t]
}

pred compareBusLocation[b : Bus, l : Location, t : Time] {
	b.location.t = l
}
